package at.fhj.ase;

import java.math.BigDecimal;
//@ model import org.jmlspecs.*;


public class ShoppingCartPos {
		
	private /*@ spec_public @*/ long posNr;
	private /*@ spec_public @*/ Article article;
	private /*@ spec_public @*/ long quantity;
	private /*@ spec_public @*/ BigDecimal pricePerUnit = new BigDecimal("0");
	
	
	public ShoppingCartPos(final long posNr, final Article article, 
			final BigDecimal pricePerUnit, long quantity) {
		setPosNr(posNr);
		setArticle(article);
		setPricePerUnit(pricePerUnit);
		setQuantity(quantity);
	}
	
	public BigDecimal getTotalPrice() {
		return new BigDecimal(this.quantity).multiply(this.pricePerUnit);
	}
	
	/*@ protected normal_behavior
	  @ 	requires posNr >= 0;
	  @ also protected exceptional_behavior
	  @		requires posNr < 0;
	  @		signals_only IllegalArgumentException;
	 */
	protected final void setPosNr(final long posNr) 
			throws IllegalArgumentException{
		if(posNr < 0) {
			throw new IllegalArgumentException("posNr must not be < 0");
		}
		this.posNr = posNr;
	}
	
	//@ ensures \result == posNr;
	protected final long getPosNr() {
		return posNr;
	}
	
	/*@ protected normal_behavior
	  @ 	requires article != null;
	  @ also protected exceptional_behavior
	  @		requires article == null;
	  @ 	signals_only NullPointerException;
	 */
	protected final void setArticle(Article article) 
			throws NullPointerException {
		if(article == null) {
			throw new NullPointerException("article must not be null");
		}
		this.article = article;
	}
	
	//@ ensures \result == article;
	protected final Article getArticle() {
		return article;
	}

	/*@ protected normal_behavior
	  @		requires quantity > 0;
	  @ also protected exceptional_behavior
	  @		requires quantity <= 0;
	  @		signals_only IllegalArgumentException; 
	 */
	protected final void setQuantity(long quantity) 
			throws IllegalArgumentException{
		if(quantity <= 0) {
			throw new IllegalArgumentException("quantity must not be <= 0");
		}
		this.quantity = quantity;
	}

	//@ ensures \result == quantity;
	protected final long getQuantity() {
		return quantity;
	}

	/*@ protected normal_behavior
	  @		requires pricePerUnit != null;
	  @		requires pricePerUnit.compareTo(new BigDecimal("0")) == 1; 
	  @ also protected exceptional_behavior
	  @		requires pricePerUnit == null;
	  @		signals (NullPointerException);
	  @	also requires pricePerUnit.compareTo(new BigDecimal("0")) == -1;
	  @ 	signals (IllegalArgumentException);
	  @*/
	protected final void setPricePerUnit(BigDecimal pricePerUnit) 
			throws IllegalArgumentException, NullPointerException{
		if(pricePerUnit == null) {
			throw new NullPointerException("pricePerUnit must not be null");
		}
		if(pricePerUnit.compareTo(new BigDecimal("0")) == -1) {
			throw new IllegalArgumentException("pricePerUnit must not be < 0");
		}
		this.pricePerUnit = pricePerUnit;
	}

	//@ ensures \result == pricePerUnit;
	protected final BigDecimal getPricePerUnit() {
		return pricePerUnit;
	}
	
	//@ also ensures \result != null;
	public String toString() {
		StringBuilder s = new StringBuilder();
		s.append(new Long(getPosNr()).toString()).append(",").append(new Long(article.getArtNr()).toString()).append(",").append(article.getName()).append(",").append(article.getDescription()).append(",");
		s.append(article.getPricePerUnit().toString()).append(",").append(this.getPricePerUnit().toString()).append(",").append(new BigDecimal(getQuantity()).toString()).append(",").append(this.getTotalPrice().toString());
		return s.toString();
	}




	
	


	
}
